several theorems about graphs#125
Conversation
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
|
OK, I should have realized that the operators must be renamed in the test module for the tests to work. |
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
|
@lemmy could you please have a look? I'd be particularly interested in your comments on my changes to existing operators. |
|
LGTM. However, wouldn't it be better to override the new generic operators using Java module overrides instead of introducing separate MC* definitions? That would free users from redefining the operators while still giving TLC an efficient definition, and follow the same approach already used elsewhere in this repository. |
|
Agreed, will try to do that. |
|
I will open a new draft PR soon with the three overrides. |
|
Also note that the definition of |
The amended definition now differs from https://github.com/tlaplus/Examples/blob/47b0e2cc0268836b89f5ce451f38e5df5f1cf773/specifications/SpecifyingSystems/AdvancedExamples/Graphs.tla#L29-L33. Perhaps, we should also amend SS def? Also, we should check if https://github.com/tlaplus/Examples/blob/master/specifications/ewd687a/EWD687a_proof.tla#L789 still proves and TLC continues to check the corresponding spec. |
|
Oh, I had not realized that Graphs was part of Specifying Systems ... As for EWD687a, I have a complete proof of the safety property (amended for the changed definition of IsTreeWithRoot) and will open a PR as soon as this one is settled. |
|
@muenchnerkindl Are you also going to align the defs in https://github.com/tlaplus/CommunityModules/blob/master/modules/UndirectedGraphs.tla? |
2 participants
This PR adds a number of theorems about graphs, including those required for the safety proof of the Dijkstra-Scholten algorithm (https://github.com/tlaplus/Examples/tree/master/specifications/ewd687a). I'll do a PR for that proof once these theorems are in.
Besides changing some (LOCAL) INSTANCE to EXTENDS due to current limitations of the PM – including in some modules imported here – I also made a few changes to Graphs.tla:
SimplePathand renamed the old definition toMCSimplePath: it applies only to finite graphs but can be evaluated by TLC,AreConnectedInandIsStronglyConnected,IsTreeWithRootso that it requires the root to be a node in the graph: the previous definition was vacuously true for an graph with an empty set of nodes, for any root, and this requires case distinctions when adding a new leaf to a tree. IMHO the present definition is reasonable and more uniform.The above changes may break some existing specification projects in that
SimplePathshould be overridden byMCSimplePathetc. when using TLC.I also noticed that the definition of
TransitiveClosureinRelations.tlais correct only for finite relations and suggest to eventually make analogous changes there, introducing an operatorMCTransitiveClosure.